KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmp4Y9DEP/rpm-lazy.xml









The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 3734 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

rpm_t_m_2#1(f_p(snd, x(x2)), x3) → Leaf(snd#2(x#1(x2, bot[2]), bot[3]))

rpm_t_m_9#1(fst, P(rpm_t_m_9(x4, x6, x8), x2), x5, x3) → Node(rpm_t_m_9#1(x4, x6, x8, bot[5]), fst#2(x5, bot[6]))

rpm_t_m_9#1(fst, P(rpm_t_m_2(x4), x2), x5, x3) → Node(rpm_t_m_2#1(x4, bot[5]), fst#2(x5, bot[6]))

rpm_t_m_8#1(x3, x2, x1) → P(rpm_t_m_9(fst, x3, x2), rpm_t_m_10(x3, x2))

rpm#3(Leaf(x8), f_p(x12, x16), x4) → P(rpm_t_m_2(f_p(x12, x16)), rpm_t_m_3(x8))

rpm#3(Node(x8, x6), f_p(x2, x4), x10) → rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)

cond_fst_p#1(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)

cond_fst_p#1(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)

fst#2(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)

fst#2(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)

snd#2(P(x18, rpm_t_m_3(x14)), x18) → x14

snd#2(P(x2, rpm_t_m_10(x6, x4)), x2) → min#2(snd#2(x6, bot[7]), snd#2(x4, bot[8]))

min#2(0, x12) → 0

min#2(S(x16), 0) → 0

min#2(S(x4), S(x2)) → S(min#2(x4, x2))

x#1(f(x4), x3) → rpm#3(x4, f_p(snd, x(f(x4))), bot[11])

main(x1) → cond_fst_p#1(x#1(f(x1), bot[0]), bot[1])

Rewrite Strategy: INNERMOST




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
rpm#3(Node(x8, x6), f_p(x2, x4), x10) →+ rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x8 / Node(x8, x6)].
The result substitution is [x10 / bot[9]].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

rpm_t_m_2#1(f_p(snd, x(x2)), x3) → Leaf(snd#2(x#1(x2, bot[2]), bot[3]))

rpm_t_m_9#1(fst, P(rpm_t_m_9(x4, x6, x8), x2), x5, x3) → Node(rpm_t_m_9#1(x4, x6, x8, bot[5]), fst#2(x5, bot[6]))

rpm_t_m_9#1(fst, P(rpm_t_m_2(x4), x2), x5, x3) → Node(rpm_t_m_2#1(x4, bot[5]), fst#2(x5, bot[6]))

rpm_t_m_8#1(x3, x2, x1) → P(rpm_t_m_9(fst, x3, x2), rpm_t_m_10(x3, x2))

rpm#3(Leaf(x8), f_p(x12, x16), x4) → P(rpm_t_m_2(f_p(x12, x16)), rpm_t_m_3(x8))

rpm#3(Node(x8, x6), f_p(x2, x4), x10) → rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)

cond_fst_p#1(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)

cond_fst_p#1(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)

fst#2(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)

fst#2(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)

snd#2(P(x18, rpm_t_m_3(x14)), x18) → x14

snd#2(P(x2, rpm_t_m_10(x6, x4)), x2) → min#2(snd#2(x6, bot[7]), snd#2(x4, bot[8]))

min#2(0', x12) → 0'

min#2(S(x16), 0') → 0'

min#2(S(x4), S(x2)) → S(min#2(x4, x2))

x#1(f(x4), x3) → rpm#3(x4, f_p(snd, x(f(x4))), bot[11])

main(x1) → cond_fst_p#1(x#1(f(x1), bot[0]), bot[1])

S is empty.
Rewrite Strategy: INNERMOST




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
Innermost TRS:
Rules:
rpm_t_m_2#1(f_p(snd, x(x2)), x3) → Leaf(snd#2(x#1(x2, bot[2]), bot[3]))
rpm_t_m_9#1(fst, P(rpm_t_m_9(x4, x6, x8), x2), x5, x3) → Node(rpm_t_m_9#1(x4, x6, x8, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_9#1(fst, P(rpm_t_m_2(x4), x2), x5, x3) → Node(rpm_t_m_2#1(x4, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_8#1(x3, x2, x1) → P(rpm_t_m_9(fst, x3, x2), rpm_t_m_10(x3, x2))
rpm#3(Leaf(x8), f_p(x12, x16), x4) → P(rpm_t_m_2(f_p(x12, x16)), rpm_t_m_3(x8))
rpm#3(Node(x8, x6), f_p(x2, x4), x10) → rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)
cond_fst_p#1(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
cond_fst_p#1(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
snd#2(P(x18, rpm_t_m_3(x14)), x18) → x14
snd#2(P(x2, rpm_t_m_10(x6, x4)), x2) → min#2(snd#2(x6, bot[7]), snd#2(x4, bot[8]))
min#2(0', x12) → 0'
min#2(S(x16), 0') → 0'
min#2(S(x4), S(x2)) → S(min#2(x4, x2))
x#1(f(x4), x3) → rpm#3(x4, f_p(snd, x(f(x4))), bot[11])
main(x1) → cond_fst_p#1(x#1(f(x1), bot[0]), bot[1])

Types:
rpm_t_m_2#1 :: f_p → bot[5]:bot[6]:bot[1] → Leaf:Node
f_p :: snd → x → f_p
snd :: snd
x :: f → x
Leaf :: 0':S → Leaf:Node
snd#2 :: P → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8] → 0':S
x#1 :: f → bot[2]:bot[0] → P
bot[2] :: bot[2]:bot[0]
bot[3] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
rpm_t_m_9#1 :: fst → P → P → bot[5]:bot[6]:bot[1] → Leaf:Node
fst :: fst
P :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8] → rpm_t_m_10:rpm_t_m_3 → P
rpm_t_m_9 :: fst → P → P → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
Node :: Leaf:Node → Leaf:Node → Leaf:Node
bot[5] :: bot[5]:bot[6]:bot[1]
fst#2 :: P → bot[5]:bot[6]:bot[1] → Leaf:Node
bot[6] :: bot[5]:bot[6]:bot[1]
rpm_t_m_2 :: f_p → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
rpm_t_m_8#1 :: P → P → bot[9]:bot[10]:bot[11] → P
rpm_t_m_10 :: P → P → rpm_t_m_10:rpm_t_m_3
rpm#3 :: Leaf:Node → f_p → bot[9]:bot[10]:bot[11] → P
rpm_t_m_3 :: 0':S → rpm_t_m_10:rpm_t_m_3
bot[9] :: bot[9]:bot[10]:bot[11]
bot[10] :: bot[9]:bot[10]:bot[11]
cond_fst_p#1 :: P → bot[5]:bot[6]:bot[1] → Leaf:Node
min#2 :: 0':S → 0':S → 0':S
bot[7] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
bot[8] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
0' :: 0':S
S :: 0':S → 0':S
f :: Leaf:Node → f
bot[11] :: bot[9]:bot[10]:bot[11]
main :: Leaf:Node → Leaf:Node
bot[0] :: bot[2]:bot[0]
bot[1] :: bot[5]:bot[6]:bot[1]
hole_Leaf:Node1_7 :: Leaf:Node
hole_f_p2_7 :: f_p
hole_bot[5]:bot[6]:bot[1]3_7 :: bot[5]:bot[6]:bot[1]
hole_snd4_7 :: snd
hole_x5_7 :: x
hole_f6_7 :: f
hole_0':S7_7 :: 0':S
hole_P8_7 :: P
hole_bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]9_7 :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
hole_bot[2]:bot[0]10_7 :: bot[2]:bot[0]
hole_fst11_7 :: fst
hole_rpm_t_m_10:rpm_t_m_312_7 :: rpm_t_m_10:rpm_t_m_3
hole_bot[9]:bot[10]:bot[11]13_7 :: bot[9]:bot[10]:bot[11]
gen_Leaf:Node14_7 :: Nat → Leaf:Node
gen_0':S15_7 :: Nat → 0':S




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
snd#2, rpm_t_m_9#1, fst#2, rpm#3, min#2
They will be analysed ascendingly in the following order:
min#2 < snd#2
rpm_t_m_9#1 = fst#2




(8) Obligation:
Innermost TRS:
Rules:
rpm_t_m_2#1(f_p(snd, x(x2)), x3) → Leaf(snd#2(x#1(x2, bot[2]), bot[3]))
rpm_t_m_9#1(fst, P(rpm_t_m_9(x4, x6, x8), x2), x5, x3) → Node(rpm_t_m_9#1(x4, x6, x8, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_9#1(fst, P(rpm_t_m_2(x4), x2), x5, x3) → Node(rpm_t_m_2#1(x4, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_8#1(x3, x2, x1) → P(rpm_t_m_9(fst, x3, x2), rpm_t_m_10(x3, x2))
rpm#3(Leaf(x8), f_p(x12, x16), x4) → P(rpm_t_m_2(f_p(x12, x16)), rpm_t_m_3(x8))
rpm#3(Node(x8, x6), f_p(x2, x4), x10) → rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)
cond_fst_p#1(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
cond_fst_p#1(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
snd#2(P(x18, rpm_t_m_3(x14)), x18) → x14
snd#2(P(x2, rpm_t_m_10(x6, x4)), x2) → min#2(snd#2(x6, bot[7]), snd#2(x4, bot[8]))
min#2(0', x12) → 0'
min#2(S(x16), 0') → 0'
min#2(S(x4), S(x2)) → S(min#2(x4, x2))
x#1(f(x4), x3) → rpm#3(x4, f_p(snd, x(f(x4))), bot[11])
main(x1) → cond_fst_p#1(x#1(f(x1), bot[0]), bot[1])

Types:
rpm_t_m_2#1 :: f_p → bot[5]:bot[6]:bot[1] → Leaf:Node
f_p :: snd → x → f_p
snd :: snd
x :: f → x
Leaf :: 0':S → Leaf:Node
snd#2 :: P → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8] → 0':S
x#1 :: f → bot[2]:bot[0] → P
bot[2] :: bot[2]:bot[0]
bot[3] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
rpm_t_m_9#1 :: fst → P → P → bot[5]:bot[6]:bot[1] → Leaf:Node
fst :: fst
P :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8] → rpm_t_m_10:rpm_t_m_3 → P
rpm_t_m_9 :: fst → P → P → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
Node :: Leaf:Node → Leaf:Node → Leaf:Node
bot[5] :: bot[5]:bot[6]:bot[1]
fst#2 :: P → bot[5]:bot[6]:bot[1] → Leaf:Node
bot[6] :: bot[5]:bot[6]:bot[1]
rpm_t_m_2 :: f_p → bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
rpm_t_m_8#1 :: P → P → bot[9]:bot[10]:bot[11] → P
rpm_t_m_10 :: P → P → rpm_t_m_10:rpm_t_m_3
rpm#3 :: Leaf:Node → f_p → bot[9]:bot[10]:bot[11] → P
rpm_t_m_3 :: 0':S → rpm_t_m_10:rpm_t_m_3
bot[9] :: bot[9]:bot[10]:bot[11]
bot[10] :: bot[9]:bot[10]:bot[11]
cond_fst_p#1 :: P → bot[5]:bot[6]:bot[1] → Leaf:Node
min#2 :: 0':S → 0':S → 0':S
bot[7] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
bot[8] :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
0' :: 0':S
S :: 0':S → 0':S
f :: Leaf:Node → f
bot[11] :: bot[9]:bot[10]:bot[11]
main :: Leaf:Node → Leaf:Node
bot[0] :: bot[2]:bot[0]
bot[1] :: bot[5]:bot[6]:bot[1]
hole_Leaf:Node1_7 :: Leaf:Node
hole_f_p2_7 :: f_p
hole_bot[5]:bot[6]:bot[1]3_7 :: bot[5]:bot[6]:bot[1]
hole_snd4_7 :: snd
hole_x5_7 :: x
hole_f6_7 :: f
hole_0':S7_7 :: 0':S
hole_P8_7 :: P
hole_bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]9_7 :: bot[3]:rpm_t_m_9:rpm_t_m_2:bot[7]:bot[8]
hole_bot[2]:bot[0]10_7 :: bot[2]:bot[0]
hole_fst11_7 :: fst
hole_rpm_t_m_10:rpm_t_m_312_7 :: rpm_t_m_10:rpm_t_m_3
hole_bot[9]:bot[10]:bot[11]13_7 :: bot[9]:bot[10]:bot[11]
gen_Leaf:Node14_7 :: Nat → Leaf:Node
gen_0':S15_7 :: Nat → 0':S
Generator Equations:
gen_Leaf:Node14_7(0) ⇔ Leaf(0')
gen_Leaf:Node14_7(+(x, 1)) ⇔ Node(Leaf(0'), gen_Leaf:Node14_7(x))
gen_0':S15_7(0) ⇔ 0'
gen_0':S15_7(+(x, 1)) ⇔ S(gen_0':S15_7(x))
The following defined symbols remain to be analysed:
rpm#3, snd#2, rpm_t_m_9#1, fst#2, min#2
They will be analysed ascendingly in the following order:
min#2 < snd#2
rpm_t_m_9#1 = fst#2